課程大綱

課程資訊

課程名稱

中階邏輯
INTERMEDIATE LOGIC

開課學期

98-1

授課對象

文學院哲學系

授課教師

楊金穆

課號

Phl4089

課程識別碼

104E12900

班次

學分

全/半年

半年

必/選修

必修

上課時間

星期五6,7,8(13:20~16:20)

上課地點

共407

備註

本課程以英語授課。群組課程請參閱必修科目資料表。
總人數上限：45人

課程簡介影片

核心能力關聯

核心能力與課程規劃關聯圖

課程大綱

為確保您我的權利,請尊重智慧財產權及不得非法影印

課程概述

This course is in essence an intermediate-level course for formal logic. I shall hence assume that the student has a nodding acquaintance with topics in Elementary Logic. Some basic knowledge of Elementary Set Theory is extremely helpful though not essential. I shall confine this course to the four main styles of formal systems for propositional logic (i.e., CPC) and predicate logic (i.e., CQC):

(a) Hilbert-Frege style (axiom) systems,
(b) Systems of natural deduction,
(c) (Formal) tableaux systems, and
(d) Sequent calculi.

課程目標

Introduce the four main formal systems, and show the relative theorem in detail.

課程要求

預期每週課後學習時數

Office Hours

指定閱讀

Lecture Note

參考書目

For overall:

J. Barwise (ed.), Handbook of Mathematical Logic, Amsterdam: North-Holland, 1977.
D. Bostock, Intermediate Logic, Oxford: Clarendon Press, 1997.
D. Scott, et. al., Notes on the Formalization of Logic, Sub-faculty of Philosophy, Oxford University, 1981.
G(a0c9)ran Sundholm, ‘Systems of deduction’ (Chapter 1.2 of Handbook of Philosophical Logic).

For axiom systems:

A. G. Hamilton, Logic for Mathematicians, Cambridge: Cambridge University Press, 1988, Chapters 1-4 and sections 1, 2 of Chapter 5.

For systems of natural deduction with the derivations set out linearly:

E. J. Lemmon, Beginning Logic, Chapman and Hall, 1965.

For systems of natural deduction with the derivations set out diagrammatically:

D. van Dalen, Logic and Structure, 3rd edition, Springer-Verlag, New York, 1994.
N. W. Tennant, Natural Logic, Edinburgh University Press, 1978.

For systems of formal tableaux:

R. C. Jeffrey, Formal Logic: Its scope and limits, 3rd ed., McGraw-Hill, Inc., 1991.
R. M. Smullyan, First-order Logic, New York: Dover Publication, Inc., 1995; original edition by Springer-Verlag, New York, 1968.

For sequent calculi:

There is no particular logic textbook adopting this system; but one can find some version of this type in some introductory books to other branches of formal logic, e.g. G. Takeuti, Proof Theory, (2nd ed., North Holland), 1987, Chapter One.

評量方式
(僅供參考)

No.	項目	百分比	說明
1.	Weekly Assignments	60%
2.	Final Exam	40%

課程進度

週次	日期	單元主題
第1週	9/18	Introduction 1 A formal language suitable for propositional logic and the standard (classical) semantics —A formal LK suitable for propositional logic: alphabet; connectives, formation rules —Polish notations for propositional language —Some basic syntactic properties of LK —Arguments by cases, proofs by induction —The standard (classical) semantics for LK: structures, truth-tables for connectives and semantic sequents; semantic inconsistency, entailment relation and counterexamples; Boolean structures and semantics, test the validity of LK-sequents —Some general properties of semantic entailments —Substitution theorem and logical equivalence; congruence theorem; duality theorem
第2週	9/25	2 Some semantic metatheorems for propositional logic —Truth-functions, expressive adequacy of LK and functional completeness theorem —Disjunctive normal form (DNF), conjunctive normal form (CNF), the interpolation theorem —Compactness and decidability of LK
第3週	10/02	3 The construction of formal systems: A survey —Axioms, assumptions, transformation rules (structural rules and rules of inferences), and derivations —Some basic syntactic properties of formal systems: structural rules, rules of inference, consistency and inconsistency —Soundness of formal systems and general approach to proof of the soundness theorem —Completeness of formal systems and a sketch of the Henkin-style proof —G(a0c9)del's incompleteness theorems
第4週	10/09	4 (Hilbert-Frege style) Axiomatic systems for propositional logic —The characteristics of axiom systems —An axiom system H for propositional logic —The deduction theorem (DT) —The soundness theorem for H —The completeness theorem for H: Post's proof, Kalmar's proof and Henkin's proof —The independence of axioms
第5週	10/16	5 Systems of natural deduction for propositional logic —Motivation for natural deduction —The characteristics of systems of natural deduction: introduction rules and elimination rules —The prototype of formal systems of natural deduction: The system N —Rules for negation and local-completeness of rules of inference for connectives —Some current systems of natural deduction for propositional logic
第6週	10/23	6 Systems of formal tableaux for propositional logic —Preliminaries: tableaux and formal tableaux systems —A tableaux system for propositional logic, soundness and completeness —The logical significance of open branches: counterexamples, entailment relations —Structural rules and derived rules in tableaux systems —Systems of formal tableaux with signed formulae
第7週	10/30	7 Sequent calculi for propositional logic —Gentzen's sequents and axiomatization of entailment relations —A sequent calculus SN with rules corresponding to a system of natural deduction —A sequent calculus ST with rules corresponding to tableau rules —Gentzen's sequent calculus SG —Gentzen's cut-free sequent calculus S —Equivalence of sequent calculi and tableau systems
第8週	11/06	8 First-order languages and semantics for predicate logic —Elements of first-order languages —A na(a0c8)ve first-order language LQ suitable for predicate logic —Preliminary to appropriate semantics for predicate logic —Substitutional interpretation of quantification: structures and semantic rules for quantifiers —Objectual interpretation of quantification: structures and basic semantics —I-equivalent-structure based semantics for LQ: i-equivalent interpretation and semantic rules for quantifiers —E-structure based semantics for LQ: the expansion of M and semantic rules for quantifiers —Semantic entailment, validity and inconsistency —Truth values in structures with the empty domain
第9週	11/13	Midterm Break
第10週	11/20	9 A Tarskian semantics for predicate logic and some general properties —A more useful first-order language LC with identity for predicate logic —A Tarskian semantics for LC —Some semantic theorems concerning identity; the substitution lemma for LC —Prenex normal form (PNF) —Decidability of first-order languages: monadic predicate formulae and -formulae —General properties of predicate logic and counterexample —Skolemization: Skolem functions, Skolemized form and Skolem axioms
第11週	11/27	10 Axiom systems for predicate logic —Axioms and rules of inference for quantified formulae —Axioms for identity —An axiomatic system for predicate logic HQ and some metatheorems —A Henkin-style proof of the completeness theorem for HQ —Independence of the axioms for quantified formulae in HQ
第12週	12/04	11 Systems of natural deduction for predicate logic —A system of natural deduction for predicate logic NQ —The equivalence between axiom systems and systems of natural deduction for predicate logic —Cuts and conversions of derivations in systems of natural deduction —The cut-elimination theorem: Normalization of natural deduction (Hauptsatz)
第13週	12/11	12 Systems of formal tableaux for predicate logic —Tableau rules for quantifiers —Tableau rules for identity —Counterexamples —Some metatheorems of the system TQ: Soundness Theorem and Completeness Theorem —A system of formal tableaux with signed formulae for predicate logic
第14週	12/18	13 Sequent calculi for predicate logic —A sequent calculus for predicate logic with rules corresponding to a natural deduction system —A sequent calculus for predicate logic with rules corresponding to a tableaux system —Gentzen’s cut-free sequent calculus for predicate logic —Gentzen’s sequent calculus for predicate logic with cut-rule SC —Cut-elimination theorem, normalization for tableau systems and sequent calculi
第15週	12/25	14 Beyond first-order logic: First-order theory and second-order logic —Pure logic vs. applied logic —A formulation of first-order arithmetic (formal number theory) —Second-order logic —Many-sorted first-order logic —Second-order logic and infinitary logic L\|
第16週	1/01	15 Free logic and inclusive logic —Russellian worlds and truth-value gaps —Elimination of truth-value gaps: free semantics, the dismissal of names, a syntactic treatment —An axiom system of free logic FC —A system of formal tableau for inclusive logic
第17週	1/08	Final Exam